es:event_system{i:l}, x:Id, e:es-E(es).
(es-isconst(es; loc(e); x))
 (t,t':rationals.
 (es-state-ap(es_state_when(es; e); x)(t)
 (=
 (es-state-ap(es_state_when(es; e); x)(t')
 ( es-vartype(es; loc(e); x))
  (es-state-ap(es_state_after(es; e); x)(t)
  (=
  (es-state-ap(es_state_after(es; e); x)(t')
  ( es-vartype(es; loc(e); x))) 

latex

Definitions	t  T, x:A. B(x), constant_function(f; A; B), rationals, es_state_after(es; e), es-state-ap(s; x), f(a), <a, b>, es-vartype(es; i; x), s = t, es_state_when(es; e), P  Q, x:A  B(x), guard(T), void, x:AB(x), P  Q, loc(e), es-isconst(es; i; x), b, es-E(es), Id, event_system{i:l},
Lemmas	es-discrete-const, event system wf, Id wf, es-E wf, assert wf, es-isconst wf, es-loc wf, rationals wf